Nuprl Lemma : pairwise-singleton
11,40
postcript
pdf
P
,
v
:Top. (
x
,
y
[
v
].
P
(
x
,
y
))
True
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
(
x
,
y
L
.
P
(
x
;
y
))
,
True
,
||
as
||
,
Y
,
P
&
Q
,
P
Q
,
P
Q
,
t
T
,
{
i
..
j
}
,
Lemmas
int
seg
wf
,
true
wf
,
top
wf
origin
P, v:Top. (x,y
[v]. P(x,y)) 
True P, v:Top. (x,y[v]. P(x,y)) True x:A. B(x) Qx,yL. P(x;y)) Q Q T
}